FDL - Nuprl Lemma : fifo+switch

Nuprl Lemma : fifo+switch_wf

11,40

postcript pdf

es:ES, C:Type, S1, S2, Ack1, Ack2:(C

), Req1, Req2:(C

).
switch between fifo+ send S1(j,i,e)
switch between fifo+ srequest Req1(i,e)
switch between fifo+ sacknowledge Ack1(j,i,e) and
switch between fifo+ send S2(j,i,e) request Req2(i,e) acknowledge Ack2(j,i,e)

latex

Definitions fifo+switch, A c B, s = t, ES, A, e c e', x(s1,s2), P Q, x:A. B(x), {x:A| B(x)} , E, x(s1,s2,s3), f(a), , Type, P & Q, x:A B(x), (e < e'), x:A. B(x), x:AB(x), t T

Lemmas es-causl wf, es-E wf, es-causle wf, not wf, event system wf

origin

Definitions	fifo+switch, A c B, s = t, ES, A, e c e', x(s1,s2), P Q, x:A. B(x), {x:A\| B(x)} , E, x(s1,s2,s3), f(a), , Type, P & Q, x:A B(x), (e < e'), x:A. B(x), x:AB(x), t T
Lemmas	es-causl wf, es-E wf, es-causle wf, not wf, event system wf